package analisis;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;
import java.util.Stack;

import reticulado.AbstractNode;
import reticulado.EjeR;
import reticulado.EjeW;
import reticulado.InsideNode;
import reticulado.LoadNode;
import reticulado.NullNode;
import reticulado.ParameterNode;
import reticulado.PointsToGraph;
import soot.Local;
import soot.SootField;
import soot.Unit;
import soot.Value;
import soot.ValueBox;
import soot.jimple.IdentityStmt;
import soot.jimple.InvokeStmt;
import soot.jimple.NullConstant;
import soot.jimple.ParameterRef;
import soot.jimple.Stmt;
import soot.jimple.ThisRef;
import soot.jimple.internal.AbstractInstanceFieldRef;
import soot.jimple.internal.JAssignStmt;
import soot.jimple.internal.JInvokeStmt;
import soot.jimple.internal.JNewExpr;
import soot.tagkit.LineNumberTag;
import soot.toolkits.graph.DirectedGraph;
import soot.toolkits.scalar.ForwardFlowAnalysis;

public class IntraProceduralAnalysis extends ForwardFlowAnalysis<Unit, PointsToGraph> {

    protected InterproceduralKInfiniteAnalysis inter;
    protected PointsToGraph ptgEntrada;
    protected Mapping mapping;
	private Stack<String> callString;

    public IntraProceduralAnalysis(DirectedGraph<Unit> graph,
            InterproceduralKInfiniteAnalysis inter,
            PointsToGraph ptgEntrada,
            Mapping mapping,
            Stack<String> callString) {
        super(graph);
        this.inter = inter;
        this.ptgEntrada = ptgEntrada;
        this.mapping = mapping;
        this.callString = callString;
        doAnalysis();
    }

    // PASO 2: definir la aproximacion (en este caso may)
    @Override
    protected void merge(PointsToGraph inSet1, PointsToGraph inSet2, PointsToGraph outSet) {
        inSet1.union(inSet2, outSet);
    }

    @Override
    protected void copy(PointsToGraph srcSet, PointsToGraph destSet) {
        destSet.copy(srcSet);
    }

    // PASO 3: definir la funcion de transferencia
    @Override
    protected void flowThrough(PointsToGraph in, Unit node, PointsToGraph out) {
        Stmt stmt = (Stmt) node;
        out.copy(in);

        if (stmt instanceof IdentityStmt ||
                stmt instanceof JAssignStmt ||
                stmt instanceof JInvokeStmt) {
            // this = @this
            if (stmt instanceof IdentityStmt) {
                IdentityStmt identity = (IdentityStmt) stmt;
                kill(in, identity, out);
                gen(out, identity);
            }
            // value = value;
            if (stmt instanceof JAssignStmt) {
                JAssignStmt asignacion = (JAssignStmt) stmt;
                kill(in, asignacion, out);
                gen(out, asignacion);
            }
            // a0.m(a1,...an)
            if (stmt instanceof InvokeStmt) {
                InvokeStmt invoc = (InvokeStmt) stmt;
                if (inter == null) {
                    out.agregarProblema(invoc);
                } else {
                    inter.analyseCall(in, invoc, out);
                }
            }
        }
    }

    protected void kill(PointsToGraph in, JAssignStmt stmt, PointsToGraph out) {

        Value vleft = stmt.getLeftOp();
        Value vright = stmt.getRightOp();

        if (vleft instanceof Local) {
            Local x = (Local) vleft;
            //x = y
            if (vright instanceof Local) {
                Local y = (Local) vright;
                // miro que no sea el caso x=x
                if (!y.equals(x)) {
                    out.definir(x, new HashSet<AbstractNode>());
                }
            }
            //x=new A
            if (vright instanceof JNewExpr) {
                out.definir(x, new HashSet<AbstractNode>());
            }
            // x= y.f
            if (vright instanceof AbstractInstanceFieldRef) {
                AbstractInstanceFieldRef yf = (AbstractInstanceFieldRef) vright;
                Local y = (Local) yf.getBase();
                if (!x.equals(y)) {
                    out.definir(x, new HashSet<AbstractNode>());
                }
            }
            //x=null
            if (vright instanceof NullConstant) {
                out.definir(x, new HashSet<AbstractNode>());
            }
        }
    }

    protected void kill(PointsToGraph in, IdentityStmt stmt, PointsToGraph out) {

        Value vleft = stmt.getLeftOp();

        if (vleft instanceof Local) {
            out.definir((Local) vleft, new HashSet<AbstractNode>());
        }

    }

    protected void gen(PointsToGraph out, IdentityStmt stmt) {

        Value vleft = stmt.getLeftOp();
        Value vright = stmt.getRightOp();

        // CASO expresion izquierda de la asignacion es una variable
        if (vleft instanceof Local) {
            Local v = (Local) vleft;

            // v = @this
            if (vright instanceof ThisRef) {
                if (!habilitadoAnalisisInter()) {
                    // si solo estoy haciendo analisis intra
                    ParameterNode nodoThis = new ParameterNode("this");
                    out.agregar(nodoThis);
                    out.definir(v, nodoThis);
                } else {
                    //si estoy dentro de un analisis interprocedural
                    out.definir(v, mapping.getThisNodes());
                }
            }
            // v = @parameter
            if (vright instanceof ParameterRef) {
                ParameterRef p = (ParameterRef) vright;
                if (!habilitadoAnalisisInter()) {
                    // si solo estoy haciendo analisis intra
                    ParameterNode nodoParametro = new ParameterNode(new Integer(p.getIndex()).toString());
                    out.agregar(nodoParametro);
                    out.definir(v, nodoParametro);
                } else {
                    //si estoy dentro de un analisis interprocedural
                    out.definir(v, mapping.getParameterNodes(p.getIndex()));
                }
            }
        }
    }

    protected void gen(PointsToGraph out, JAssignStmt stmt) {
        ValueBox leftBox = stmt.leftBox;
        ValueBox rightBox = stmt.rightBox;

        Value vleft = leftBox.getValue();
        Value vright = rightBox.getValue();

        // CASO expresion izquierda de la asignacion es una variable
        if (vleft instanceof Local) {
            Local x = (Local) vleft;
            // x = y (se debe cumplir x!=y)
            if (vright instanceof Local) {
                Local y = (Local) vright;
                if (!y.equivTo(x)) {
                    Set<AbstractNode> nodosReferenciados = out.alcanzados((Local) vright);
                    if (nodosReferenciados != null) {
                        out.definir(x, nodosReferenciados);
                    }
                }
            }
            // x = new A()
            if (vright instanceof JNewExpr) {
                InsideNode nodoNuevo = new InsideNode(getNuevoId(stmt));
                Set<AbstractNode> nodosAlcanzados = new HashSet<AbstractNode>();
                nodosAlcanzados.add(out.agregar(nodoNuevo));
                out.definir(x, nodosAlcanzados);
            }
            // x = y.f
            if (vright instanceof AbstractInstanceFieldRef) {
                AbstractInstanceFieldRef referenciayf = (AbstractInstanceFieldRef) vright;
                Value basey = referenciayf.getBase();
                if (basey instanceof Local) {
                    Local y = (Local) basey;
                    SootField campo = referenciayf.getField();
                    // veo si los nodos (apuntados por y) ya hicieron un load de su campo f
                    Set<AbstractNode> alcanzadosy = out.alcanzados(y);

                    //si estoy en el caso x = x.f borro las antiguas referencias de x (que son las misma que de y)
                    if (x.equivTo(y)) {
                        out.definir(x, new HashSet<AbstractNode>());
                    }

                    for (AbstractNode nodo : alcanzadosy) {
                        //busco todos los nodos apuntados desde el nodo actual por el campo f
                        Set<AbstractNode> cargados = out.nodoCargado(nodo, campo.getName());

                        if (cargados.isEmpty()) {
                            // creo un nuevo load node con su id y lo agrego
                            LoadNode nuevoNodo = new LoadNode(getNuevoId(stmt));
                            out.agregar(nuevoNodo);
                            //agrego el nuevo nodo a los alcanzables de x sin borrar los que estaban
                            out.definir(x, nuevoNodo);

                            //agrego un nuevo eje de lectura
                            Set<AbstractNode> nodosAlcanzadosY = out.alcanzados(y);
                            for (AbstractNode n : nodosAlcanzadosY) {
                                EjeR nuevoEje = new EjeR(n, campo.getName(), nuevoNodo);
                                out.agregar(nuevoEje);
                            }
                        } else {
                            //si ya hizo un load de ese campo
                            for (AbstractNode nodoCargado : cargados) {
                                out.definir(x, nodoCargado);
                            }
                        }
                    }
                }
            }
            // x = null
            if (vright instanceof NullConstant) {
                out.definir(x, NullNode.getInstance());
            }
        }

        // CASO expresion izquierda de la asignacion es un campo (x.f)
        if (vleft instanceof AbstractInstanceFieldRef) {
            AbstractInstanceFieldRef referenciaxf = (AbstractInstanceFieldRef) vleft;
            Value basex = referenciaxf.getBase();
            SootField campo = referenciaxf.getField();
            // x.f = y
            if (vright instanceof Local) {
                Local variabley = (Local) vright;
                Set<AbstractNode> Lx = out.alcanzados((Local) basex);
                Set<AbstractNode> Ly = out.alcanzados(variabley);

                for (AbstractNode nodox : Lx) {
                    for (AbstractNode nodoy : Ly) {
                        EjeW nuevoEje = new EjeW(nodox, campo.getName(), nodoy);
                        out.agregar(nuevoEje);
                    }
                }
            }
            //x.f = null
            if (vright instanceof NullConstant) {
                Set<AbstractNode> Lx = out.alcanzados((Local) basex);
                for (AbstractNode nodox : Lx) {
                    EjeW nuevoEje = new EjeW(nodox, campo.getName(), NullNode.getInstance());
                    out.agregar(nuevoEje);
                }
            }
        }
    }

    private String getNuevoId(JAssignStmt stmt) {
        String idNuevoNodo = new String();
        if (callString != null) {
            for (String call : callString) {
            	idNuevoNodo += call + "->";
            }
        }
        LineNumberTag numeroLinea = (LineNumberTag) stmt.getTag("LineNumberTag");
        idNuevoNodo += new Integer(numeroLinea.getLineNumber()).toString();
		return idNuevoNodo;
	}

	// PASO 4: definir el flujo inicial
    @Override
    protected PointsToGraph entryInitialFlow() {
        if (ptgEntrada == null) {
            return new PointsToGraph();
        } else {
            return ptgEntrada;
        }
    }

    @Override
    protected PointsToGraph newInitialFlow() {
        return new PointsToGraph();
    }

    private Boolean habilitadoAnalisisInter() {
        return ptgEntrada != null && mapping != null;
    }

    public void copyResult(PointsToGraph dst) {
        dst.clear();
        Iterator it = graph.getTails().iterator();
        while (it.hasNext()) {
            Stmt stmt = (Stmt) it.next();
            PointsToGraph ref = (PointsToGraph) getFlowAfter(stmt);
            dst.union(ref);
        }
        //r.removeLocals();
        //r.simplifyLoad();
        //r.simplifyInside();
        //r.updateStat();
    }

    public PointsToGraph getResult(){
        PointsToGraph res = new PointsToGraph();
        Iterator it = graph.getTails().iterator();
        while (it.hasNext()) {
            Stmt stmt = (Stmt) it.next();
            PointsToGraph ref = (PointsToGraph) getFlowAfter(stmt);
            res.union(ref);
        }
        return res;
    }
}
